COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	FETCH INTEGE.AX
C00004 ENDMK
C⊗;
FETCH INTEGE.AX;
∧I INDUCTION[P←λN.¬(N≥SUCC N)];
∀E PEANO1 0;
∀E GREATER2 SUCC 0;
∀E GREATER3 SUCC N SUCC SUCC N;
∀E PEANO2 N;
∀E PEANO2 SUCC N;
SUBSTR 5 IN 4;
SUBSTR 6 IN 7;
TAUT 1:#1#2#1 8;
∀I 9 N;
TAUT 1:#2 1 2 3 10;
LABEL LEMMA1 = 11;


DECLARE PREDPAR Q(NATNUM,NATNUM);
∧I INDUCTION[P←λN.(¬Q(N,0)∨Q(0,M*N)∨¬∀I K.(¬I=0 ∧ Q(I,K) ⊃ Q(PRED I,K+M)))];
∀E TIMES1 M;
TAUTEQ 12:#1#2⊃12:#2 12 13;
ASSUME ∀N.((Q(N,0)∧∀I K.((¬(I=0)∧Q(I,K))⊃Q(PRED I,K+M)))⊃Q(0,M*N));
∀E 15 SUCC N;
TAUT 14:#1#1 16;
∀I 17 N;
⊃I 15 18;
TAUT 15:⊃14:#2 14 19;
ASSUME 20:#1#1#1;
TAUT 21:#1 21;
TAUT 21:#2 21;
∧I INDUCTION[P←λN1.(N≥N1 ⊃ Q(N-N1,M*N1))];
∀E MINUS2 N;
∀E TIMES1 M;
TAUTEQ 24:#1#2⊃24:#2 22 24 25 26;
ASSUME 27:#1#1#1;
∀E 23 N-N1 M*N1;
ASSUME N≥SUCC N1;

FETCH ADHOC.THE;
∀E ADHOC1 N N1;
∀E ADHOC2 N N1;
∀E MINUS1 N N1;
TAUT 29:#2#2 28 29 30 31 32 33;
⊃I 30 34;
⊃I 28 35;
∀E TIMES3 M N1;
SUBST 37 IN 36;
∀E MINUS3 N N1;
SUBST 39 IN 38;
∀I 40 N1;
MP 27 41;
∀E 42 N;
∀E ADHOC3 N;
SUBSTR 44 IN 43;
∀E ADHOC4 N;
MP 46 45;
⊃I 21 47;
∀I 48 N;
MP 49 20;